/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ α`REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

␈↓ α∧␈↓α␈↓ εεby John McCarthy











␈↓ α∧␈↓␈↓ αTThis␈αpaper␈αpresents␈αmethods␈αof␈αrepresenting␈αrecursive␈αprograms␈αby␈αsentences␈αand␈αschemata
␈↓ α∧␈↓of␈α
first␈α
order␈α
logic,␈α
characterization␈α
of␈α
␈↓↓recursion␈α
induction␈↓,␈α
␈↓↓subgoal␈α
induction␈↓,␈α∞␈↓↓inductive␈α
assertions␈↓
␈↓ α∧␈↓and␈α⊂other␈α⊂ways␈α⊂of␈α⊂proving␈α⊂facts␈α⊂about␈α⊂programs␈α⊂as␈α⊂axiom␈α⊂schemata␈α⊂of␈α⊂first␈α⊂order␈α⊂logic,␈α∂and
␈↓ α∧␈↓applications of these results to proving assertions about programs.

␈↓ α∧␈↓␈↓εThis draft of FIRST.NEW[W77,JMC] PUBbed at 10:50 on September 19, 1978.␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u2


␈↓ α∧␈↓α1. Introduction and Motivation.

␈↓ α∧␈↓␈↓ αTIt␈α
has␈αbeen␈α
concluded␈αfrom␈α
the␈α
undecideability␈αof␈α
both␈αequivalence␈α
and␈αnon-equivalence␈α
of
␈↓ α∧␈↓abstract␈α⊃recursive␈α⊃program␈α⊃schemata␈α⊃that␈α⊃recursive␈α⊃programs␈α⊃cannot␈α⊃be␈α⊃characterized␈α⊃in␈α⊂first
␈↓ α∧␈↓order␈α⊂logic.␈α⊃ Cooper␈α⊂(1969)␈α⊂showed␈α⊃how␈α⊂to␈α⊂characterize␈α⊃them␈α⊂in␈α⊂second␈α⊃order␈α⊂logic,␈α⊃and␈α⊂that
␈↓ α∧␈↓seemed␈α∪to␈α∩settle␈α∪the␈α∪matter.␈α∩ However,␈α∪we␈α∩will␈α∪exhibit␈α∪first␈α∩order␈α∪characterizations␈α∪that␈α∩are
␈↓ α∧␈↓incomplete␈α∞only␈α∞in␈α∞that␈α∞they␈α∞admit␈α∞non-standard␈α∞models␈α∞like␈α∞those␈α∞of␈α∞first␈α∞order␈α∞arithmetic.␈α
 It
␈↓ α∧␈↓now␈α∂seems␈α∂likely␈α∂that␈α⊂all␈α∂"ordinary"␈α∂␈↓↓extensional␈↓␈α∂assertions␈α⊂about␈α∂programs␈α∂will␈α∂be␈α⊂provable␈α∂or
␈↓ α∧␈↓disprovable␈αin␈αfirst␈αorder␈αtheories.␈α ␈↓↓Extensional␈↓␈αassertions␈αabout␈αa␈αprogram␈αconcern␈αthe␈αfunctions
␈↓ α∧␈↓computed␈αby␈αthe␈αprogram␈αand␈αnot␈αthe␈αmanner␈αof␈αcomputation.␈α That␈αa␈αmerge␈αsort␈αprogram␈αgives
␈↓ α∧␈↓the␈αsame␈αresult␈αas␈αa␈αbubble␈αsort␈αprogram␈αis␈αan␈αextensional␈αassertion,␈αbut␈αthe␈αfact␈αthat␈αit␈αdoes␈αless
␈↓ α∧␈↓computation is not.

␈↓ α∧␈↓␈↓ αTBesides␈αilluminating␈αthe␈αlogical␈αstructure␈αof␈αcomputer␈αprograms,␈αthese␈αresults␈αhave␈αpractical
␈↓ α∧␈↓significance.␈α∪ First,␈α∀the␈α∪correctness␈α∪of␈α∀a␈α∪computer␈α∪program␈α∀often␈α∪involves␈α∪facts␈α∀about␈α∪other
␈↓ α∧␈↓mathematical␈αdomains,␈α
and␈αthese␈αare␈α
often␈αconveniently␈αexpressed␈α
in␈αfirst␈αorder␈α
logic␈αor␈αin␈α
a␈αset
␈↓ α∧␈↓theory␈αaxiomatized␈α
in␈αfirst␈α
order␈αlogic.␈α
 It␈αhas␈αproved␈α
particularly␈αdifficult␈α
to␈αwork␈α
within␈αlogics
␈↓ α∧␈↓that␈α∃admit␈α∀only␈α∃continuous␈α∀functions␈α∃and␈α∀predicates.␈α∃ Second,␈α∀proof-checking␈α∃and␈α∀theorem
␈↓ α∧␈↓proving␈αprograms␈αhave␈αbeen␈αdeveloped␈αfor␈αfirst␈αorder␈αlogic.␈α Finally,␈αfirst␈αorder␈αlogic␈αis␈αcomplete,
␈↓ α∧␈↓so␈α∞that␈α∞the␈α∂G␈↓
:␈↓odelian␈α∞incompleteness␈α∞of␈α∂any␈α∞theory␈α∞is␈α∞in␈α∂the␈α∞set␈α∞of␈α∂axioms␈α∞and␈α∞can␈α∂be␈α∞reduced
␈↓ α∧␈↓when necessary by adding axioms rather than by changing the logical system.

␈↓ α∧␈↓␈↓ αTWhile␈α↔our␈α↔goal␈α↔is␈α⊗first␈α↔order␈α↔representations␈α↔of␈α⊗recursive␈α↔programs,␈α↔we␈α↔will␈α⊗make
␈↓ α∧␈↓considerable informal use of higher order functionals and predicates.

␈↓ α∧␈↓␈↓ αTWe␈α⊗present␈α↔two␈α⊗methods␈α↔of␈α⊗representing␈α↔recursive␈α⊗programs.␈α↔ The␈α⊗first␈α↔involves␈α⊗a
␈↓ α∧␈↓␈↓↓functional␈α∞equation␈↓␈α∞and␈α∞a␈α∞␈↓↓minimization␈α∞schema␈↓␈α∞for␈α∞each␈α∞program.␈α∞ The␈α∞functional␈α∞equation␈α∞has
␈↓ α∧␈↓the␈αfunction␈αon␈αboth␈αsides␈αof␈αan␈αequality␈αsign␈αand␈αso␈αdefines␈αit␈αimplicitly.␈α However,␈αall␈αvariables
␈↓ α∧␈↓are␈α∞universally␈α∞quantified.␈α∞ Th→␈α∞second␈α∂approach␈α∞defines␈α∞the␈α∞function␈α∞explicitly,␈α∂but␈α∞existential
␈↓ α∧␈↓quantifiers␈α
asserting␈α
the␈αexistence␈α
of␈α
finite␈αapproximations␈α
to␈α
the␈αfunction␈α
occur␈α
in␈α
the␈αformula.
␈↓ α∧␈↓The␈α
fact␈α
that␈α
the␈α
functional␈α
equation␈α
of␈α
a␈α
program␈α
not␈α
known␈α
to␈α
terminate␈α
can␈α
nevertheless␈αbe
␈↓ α∧␈↓written so simply in first order logic was discovered by Cartwright (1977), but the rest seems new.


␈↓ α∧␈↓α2. Recursive Programs.

␈↓ α∧␈↓␈↓ αTAn␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ α∧␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ α∧␈↓logic are given in (Cooper 1969) and (Park 1970).

␈↓ α∧␈↓␈↓ αTWe consider ␈↓↓recursive programs␈↓ of the form

␈↓ α∧␈↓1)␈↓ αt ␈↓↓f(x) ← ␈↓	t␈↓↓[f](x)␈↓,

␈↓ α∧␈↓where ␈↓	t␈↓ is a ␈↓↓computable functional␈↓ like

␈↓ α∧␈↓2)␈↓ αt ␈↓↓␈↓	t␈↓↓ = λf.λx.(␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ x . f(x - 1))␈↓,

␈↓ α∧␈↓which gives rise to the well known recursive definition of the factorial function, namely
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u3


␈↓ α∧␈↓3)␈↓ αt ␈↓↓n! ← ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓.

␈↓ α∧␈↓␈↓ αTIn␈α
general,␈α
we␈α
shall␈α
be␈αinterested␈α
in␈α
partial␈α
functions␈α
from␈αa␈α
domain␈α
D1␈α
to␈α
a␈α
domain␈αD2.
␈↓ α∧␈↓We␈α⊃augment␈α⊂these␈α⊃domains␈α⊃by␈α⊂an␈α⊃undefined␈α⊃element␈α⊂called␈α⊃␈↓πT␈↓␈α⊃(read␈α⊂"bottom")␈α⊃giving␈α⊃rise␈α⊂to
␈↓ α∧␈↓domains␈αD1␈↓∧+␈↓␈αand␈αD2␈↓∧+␈↓.␈α A␈αset␈α␈↓↓F␈↓␈αof␈αtotal␈αbase␈αfunctions␈αon␈αthe␈αdomains␈αis␈αassumed␈αavailable,␈αand
␈↓ α∧␈↓we study functions ␈↓↓computable from the set F␈↓ as in (McCarthy 1963).

␈↓ α∧␈↓␈↓ αTIt␈αis␈αnecessary␈αto␈αdistinguish␈αbetween␈αa␈αprogram␈αas␈αa␈αtext␈αand␈αthe␈αpartial␈α
function␈αdefined
␈↓ α∧␈↓by␈α⊃the␈α⊃program␈α⊂when␈α⊃one␈α⊃is␈α⊂interested␈α⊃in␈α⊃describing␈α⊂the␈α⊃dependence␈α⊃of␈α⊂the␈α⊃function␈α⊃on␈α⊂the
␈↓ α∧␈↓interpretation␈α
of␈α
the␈α
basic␈αfunction␈α
and␈α
predicate␈α
symbols.␈α
 However,␈αwe␈α
will␈α
be␈α
working␈αwith␈α
just
␈↓ α∧␈↓one␈α
interpretation␈α
at␈αa␈α
time,␈α
so␈αwe␈α
won't␈α
use␈αseparate␈α
symbols␈α
for␈αprograms␈α
and␈α
the␈αfunctions␈α
they
␈↓ α∧␈↓determine.


␈↓ α∧␈↓α3. The Functional Equation of a Recursive Program.

␈↓ α∧␈↓␈↓ αTConsider the Lisp program

␈↓ α∧␈↓4)␈↓ αt ␈↓↓subst[x,y,z] ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t z ␈↓αthen␈↓↓ [␈↓αif␈↓↓ z=y ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z] ␈↓αelse␈↓↓ subst[x,y,␈↓αa␈↓↓ z] . subst[x,y,␈↓αd␈↓↓ z]␈↓.

␈↓ α∧␈↓The␈α
above␈α
is␈α
in␈α
Lisp␈α
␈↓↓external␈↓␈α
or␈α
␈↓↓publication␈↓␈α
notation␈α
in␈α
which␈α
 ␈↓αa␈↓ ␈↓↓x␈↓ ␈α
(bold␈α
face␈α
␈↓αa␈↓)␈α
stands␈α
for␈α
␈↓↓car[x]␈↓,
␈↓ α∧␈↓ ␈↓αd␈↓ ␈↓↓x␈↓ ␈α∂for␈α⊂␈↓↓cdr[x]␈↓,␈α∂ ␈↓↓x . y␈↓ ␈α∂for␈α⊂␈↓↓cons[x,y]␈↓,␈α∂ ␈↓αa␈↓t ␈↓↓x␈↓ ␈α⊂for␈α∂␈↓↓atom[x]␈↓,␈α∂ ␈↓αn␈↓ ␈↓↓x␈↓ ␈α⊂for␈α∂␈↓↓null[x]␈↓,␈α∂and␈α⊂␈↓↓<x␈↓β1␈↓↓␈α∂...␈α⊂x␈↓βn␈↓>␈α∂for
␈↓ α∧␈↓␈↓↓list[x␈↓β1␈↓↓,␈α
...␈α
,x␈↓βn␈↓],␈α
and␈α
␈↓↓x * y␈↓␈α
for␈α
␈↓↓append[x,y]␈↓.␈α
 Equality␈α
is␈α
taken␈α
as␈α
equality␈α
of␈α
S-expressions␈αso␈α
that
␈↓ α∧␈↓␈↓αeq␈↓ is not used.  The program is written

␈↓ α∧␈↓␈↓ αT(DE␈αSUBST␈α(X␈αY␈αZ)␈α(COND␈α((ATOM␈αZ)␈α(COND␈α((EQUAL␈αZ␈αY)␈αX)␈α(T␈αZ)))␈α(T␈α(CONS
␈↓ α∧␈↓(SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

␈↓ α∧␈↓in Lisp ␈↓↓internal notation␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α∞basic␈α
functions␈α∞{␈↓↓car,␈α
cdr,␈α∞cons,␈α
atom}␈↓␈α∞of␈α∞Lisp␈α
are␈α∞all␈α
assumed␈α∞total,␈α
but␈α∞we␈α∞will␈α
say
␈↓ α∧␈↓nothing␈α∞about␈α∞the␈α∞values␈α∞of␈α∞␈↓↓car␈↓␈α∞and␈α∞␈↓↓cdr␈↓␈α∞when␈α∞applied␈α∞to␈α∞atoms.␈α∞ According␈α∞to␈α∞the␈α∞fixed␈α∞point
␈↓ α∧␈↓theory␈α∞of␈α∞recursive␈α∞programs,␈α∞any␈α∂such␈α∞program␈α∞defines␈α∞a␈α∞function␈α∂␈↓↓f␈↓␈α∞from␈α∞␈↓↓Sexp␈↓␈α∞(the␈α∞set␈α∂of␈α∞S-
␈↓ α∧␈↓expressions)␈αto␈αSexp␈↓∧+␈↓␈α(the␈αset␈αof␈αS-expressions␈αaugmented␈αby␈α␈↓πT␈↓).␈α This␈αfunction␈αcan␈αbe␈αcomputed
␈↓ α∧␈↓by␈α∂any␈α∂␈↓↓safe␈α∞computation␈α∂rule␈↓,␈α∂(in␈α∂the␈α∞terminology␈α∂of␈α∂Manna,␈α∞Ness,␈α∂and␈α∂Vuillemin␈α∂(1973)),␈α∞and
␈↓ α∧␈↓when␈α∞the␈α∞computation␈α
terminates,␈α∞its␈α∞value␈α
will␈α∞belong␈α∞to␈α
␈↓↓Sexp.␈↓␈α∞When␈α∞the␈α∞computation␈α
doesn't
␈↓ α∧␈↓terminate,␈α∂we␈α∂postulate␈α∞␈↓↓f(x) = ␈↓πT␈↓↓␈↓.␈α∂ Although␈α∂the␈α∂particular␈α∞function␈α∂␈↓↓subst␈↓␈α∂always␈α∂terminates,␈α∞our
␈↓ α∧␈↓first␈α∂order␈α∞formula␈α∂doesn't␈α∞assume␈α∂it.␈α∞ Instead,␈α∂the␈α∞first␈α∂order␈α∞formula␈α∂(5)␈α∞below␈α∂is␈α∂the␈α∞starting
␈↓ α∧␈↓point of a structural induction proof that ␈↓↓subst␈↓ is total.

␈↓ α∧␈↓␈↓ αTThese facts show that the function ␈↓↓subst␈↓ defined recursively by (4) satisfies the sentence

␈↓ α∧␈↓5)␈↓ αt␈α⊃␈↓↓∀x␈α∩y␈α⊃z.(subst(x,y,z)␈α⊃=␈α∩␈↓αif␈↓↓␈α⊃␈↓αa␈↓↓t␈α⊃z␈α∩␈↓αthen␈↓↓␈α⊃(␈↓αif␈↓↓␈α⊃z␈α∩=␈α⊃y␈α⊃␈↓αthen␈↓↓␈α∩x␈α⊃␈↓αelse␈↓↓␈α⊃z)␈α∩␈↓αelse␈↓↓␈α⊃subst(x,y,␈↓αa␈↓↓␈α∩z)␈α⊃.
␈↓ α∧␈↓↓subst(x,y,␈↓αd␈↓↓ z))␈↓

␈↓ α∧␈↓of␈α
first␈αorder␈α
logic.␈α
 The␈αvariables␈α
␈↓↓x,␈αy␈↓␈α
and␈α
␈↓↓z␈↓␈αrange␈α
over␈α␈↓↓Sexp;␈↓␈α
when␈α
we␈αwant␈α
to␈α
quantify␈αover
␈↓ α∧␈↓␈↓↓Sexp␈↓∧+␈↓,␈α⊃we␈α⊃use␈α⊂␈↓↓X,␈α⊃Y␈α⊃␈↓and␈↓↓␈α⊂Z␈↓.␈α⊃ Moreover,␈α⊃we␈α⊂are␈α⊃augmenting␈α⊃first␈α⊂order␈α⊃logic,␈α⊃as␈α⊃described␈α⊂in
␈↓ α∧␈↓(Manna␈α1974),␈α
by␈αallowing␈αconditional␈α
expressions␈αas␈αterms.␈α
 The␈αaugmentation␈αdoes␈α
not␈αchange
␈↓ α∧␈↓what␈α∀can␈α∀be␈α∀expressed␈α∀in␈α∀first␈α∃order␈α∀logic,␈α∀because␈α∀conditional␈α∀expressions␈α∀can␈α∃always␈α∀be
␈↓ α∧␈↓eliminated from sentences by distributing predicates over them.  Thus (5) can be written
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u4


␈↓ α∧␈↓6)␈↓ αt␈α
␈↓↓∀x␈αy␈α
z.(␈↓αa␈↓↓t␈α
z␈α⊃␈α
(z=y␈α
⊃␈αsubst(x,y,z)␈α
=␈αx)␈α
∧␈α
z≠y␈α⊃␈α
subst(x,y,z)␈α
=␈αz)␈α
∧␈α
¬␈↓αa␈↓↓t␈αz␈α
⊃␈αsubst(x,y,z)␈α
=
␈↓ α∧␈↓↓subst(x,y,␈↓αa␈↓↓ z) . subst(x,y,␈↓αd␈↓↓ z)),␈↓

␈↓ α∧␈↓but␈α∪we␈α∪will␈α∪use␈α∪conditional␈α∪expressions,␈α∩because␈α∪they␈α∪are␈α∪clearer␈α∪and␈α∪express␈α∪the␈α∩recursive
␈↓ α∧␈↓program␈αdirectly.␈α
 Indeed,␈αwe␈α
recommend␈αtheir␈αuse␈α
as␈αterms␈α
in␈αlogic␈αgenerally,␈α
and␈αin␈α
first␈αorder
␈↓ α∧␈↓logic␈α∩in␈α∩particular.␈α⊃ They␈α∩don't␈α∩extend␈α∩the␈α⊃logical␈α∩power,␈α∩but␈α∩they␈α⊃permit␈α∩many␈α∩facts␈α∩to␈α⊃be
␈↓ α∧␈↓expressed without circumlocution.

␈↓ α∧␈↓␈↓ αTOne␈αgoal␈αof␈α
our␈αfirst␈αorder␈α
representation␈αis␈αto␈αuse␈α
(4)␈αonly␈αto␈α
justify␈αwriting␈α(5)␈α
and␈αthen
␈↓ α∧␈↓prove all properties of ␈↓↓subst␈↓ using a first order axiomatization of Lisp.




␈↓ α∧␈↓α4. First Order Axioms for Lisp.

␈↓ α∧␈↓␈↓ αTWe␈α⊂use␈α⊃lower␈α⊂case␈α⊂variables␈α⊃␈↓↓x,␈↓␈α⊂␈↓↓y,␈↓␈α⊃and␈α⊂␈↓↓z␈↓␈α⊂with␈α⊃or␈α⊂without␈α⊂subscripts␈α⊃to␈α⊂range␈α⊃over␈α⊂S-
␈↓ α∧␈↓expressions.␈α Capitalized␈αvariables␈αrange␈αover␈αall␈αentities.␈α
 We␈αalso␈αuse␈αvariables␈α␈↓↓u,␈↓␈α␈↓↓v␈↓␈αand␈α␈↓↓w␈↓␈α
with
␈↓ α∧␈↓or␈α∂without␈α∂subscripts␈α∂to␈α∂range␈α∂over␈α∂lists,␈α∂i.e.␈α∂S-expressions␈α∂such␈α∂that␈α∂successive␈α∂␈↓↓cdr␈↓s␈α∂eventually
␈↓ α∧␈↓reach␈αNIL.␈α (The␈α␈↓↓car␈↓␈αof␈αa␈αlist␈αis␈αnot␈αrequired␈αto␈αbe␈αa␈αlist).␈α We␈αuse␈αpredicates␈α␈↓↓issexp␈↓␈αand␈α␈↓↓islist␈↓␈αto
␈↓ α∧␈↓assert␈α∪that␈α∪an␈α∀individual␈α∪is␈α∪an␈α∀S-expression␈α∪or␈α∪a␈α∪list.␈α∀ First␈α∪come␈α∪the␈α∀"housekeeping"␈α∪and
␈↓ α∧␈↓"algebraic" axioms:

␈↓ α∧␈↓L1: ␈↓↓∀x.issexp x␈↓

␈↓ α∧␈↓L2: ␈↓↓∀u.islist u␈↓

␈↓ α∧␈↓L3: ␈↓↓∀u.issexp u␈↓

␈↓ α∧␈↓L4: ␈↓↓¬issexp ␈↓πT␈↓↓

␈↓ α∧␈↓↓L5: islist ␈↓NIL

␈↓ α∧␈↓L6: ␈↓↓␈↓αa␈↓↓t qNIL␈↓

␈↓ α∧␈↓L7: ␈↓↓∀u.(␈↓αa␈↓↓t u ⊃ u = ␈↓NIL␈↓↓)␈↓

␈↓ α∧␈↓L8: ␈↓↓∀x y.issexp (x.y)␈↓

␈↓ α∧␈↓L9: ␈↓↓∀x u.islist (x.u)␈↓

␈↓ α∧␈↓L10: ␈↓↓∀x. ¬␈↓αa␈↓↓t x ⊃ issexp ␈↓αa␈↓↓ x␈↓

␈↓ α∧␈↓L11: ␈↓↓∀x. ¬␈↓αa␈↓↓t x ⊃ issexp ␈↓αd␈↓↓ x␈↓

␈↓ α∧␈↓L12: ␈↓↓∀u. u ≠ qNIL ⊃ islist ␈↓αd␈↓↓ u␈↓

␈↓ α∧␈↓L13: ␈↓↓∀x y. ␈↓αa␈↓↓ (x.y) = x␈↓

␈↓ α∧␈↓L14: ␈↓↓∀x y. ␈↓αd␈↓↓ (x.y) = y␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u5


␈↓ α∧␈↓L15: ␈↓↓∀x y. ¬␈↓αa␈↓↓t (x.y)␈↓

␈↓ α∧␈↓L16: ␈↓↓∀x.¬␈↓αa␈↓↓t x ⊃ (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x) = x␈↓

␈↓ α∧␈↓␈↓ αTNext we have axiom schemata of induction

␈↓ α∧␈↓LS1: ␈↓↓(∀x.␈↓αa␈↓↓t x ⊃ ␈↓	F␈↓↓ x) ∧ ∀x.(¬␈↓αa␈↓↓t x ∧ ␈↓	F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ⊃ ∀x.␈↓	F␈↓↓ x␈↓

␈↓ α∧␈↓LS2: ␈↓↓(∀u.u = ␈↓NIL␈↓↓ ⊃ ␈↓	F␈↓↓ u) ∧ ∀u.(u ≠ ␈↓NIL␈↓↓ ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓	F␈↓↓ u) ⊃ ∀u. ␈↓	F␈↓↓ u␈↓.

␈↓ α∧␈↓␈↓ αTFrom these axioms and schemata, we can prove

␈↓ α∧␈↓7)␈↓ αt ␈↓↓∀x y z.issexp subst(x,y,z)␈↓

␈↓ α∧␈↓which␈α
is␈α
our␈α
way␈α
of␈α
saying␈αthat␈α
␈↓↓subst␈↓␈α
is␈α
total.␈α
 The␈α
key␈αstep␈α
is␈α
applying␈α
the␈α
axiom␈α
schema␈αLS1
␈↓ α∧␈↓with␈α∩the␈α∪predicate␈α∩␈↓↓␈↓	F␈↓↓(z)␈α∩≡␈α∪issexp␈α∩subst(x,y,z)␈↓.␈α∩ We␈α∪can␈α∩also␈α∩prove␈α∪in␈α∩first␈α∩order␈α∪logic␈α∩such
␈↓ α∧␈↓algebraic properties of ␈↓↓subst␈↓ as

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) = subst(x,y,subst(z,y1,z1)))␈↓

␈↓ α∧␈↓if␈αwe␈αhave␈αsuitable␈αaxiomatization␈αof␈αthe␈αpredicate␈α␈↓↓occur(x,y)␈↓␈αmeaning␈αthat␈αthe␈αatom␈α␈↓↓x␈↓␈αoccurs␈αin
␈↓ α∧␈↓the S-expression ␈↓↓y.␈↓

␈↓ α∧␈↓␈↓ αTThe␈α
axiomatization␈α
of␈α
the␈α
predicate␈α
␈↓↓occur␈↓␈α
raises␈α
some␈α
new␈α
problems.␈α
 It␈α
is␈α
defined␈α∞by␈α
the
␈↓ α∧␈↓recursive Lisp program

␈↓ α∧␈↓9)␈↓ αt ␈↓↓occur(x,y) ← (x = y) ∨ (¬␈↓αa␈↓↓t y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y)))␈↓.

␈↓ α∧␈↓If␈α∂we␈α∂were␈α∂sure␈α∂in␈α∞advance␈α∂that␈α∂␈↓↓occur␈↓␈α∂were␈α∂total,␈α∂we␈α∞could␈α∂translate␈α∂the␈α∂recursion␈α∂(9)␈α∂into␈α∞the
␈↓ α∧␈↓sentence

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀x y.(occur(x,y) ≡ (x = y) ∨ (¬␈↓αa␈↓↓t y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y))))␈↓

␈↓ α∧␈↓which␈α⊂will␈α∂suffice␈α⊂for␈α∂proving␈α⊂(8),␈α∂but␈α⊂we␈α∂have␈α⊂no␈α∂right␈α⊂to␈α∂write␈α⊂it␈α∂down␈α⊂from␈α⊂the␈α∂recursive
␈↓ α∧␈↓definition (9).

␈↓ α∧␈↓␈↓ αTWhat we may write without proving that ␈↓↓occur␈↓ is total is an implicit definition

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀x y.(occura(x,y) = (x equals y) or (not atom y and (occura(x,␈↓αa␈↓↓ y) or occura(x,␈↓αd␈↓↓ y))))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀x y.(occur(x,y) ≡ (occura(x,y) = T))␈↓.

␈↓ α∧␈↓From␈α∞(11),␈α∞we␈α∞can␈α∞prove␈α∞that␈α∞␈↓↓occura␈↓␈α∂is␈α∞total␈α∞by␈α∞structural␈α∞induction␈α∞and␈α∞from␈α∞this␈α∂(10)␈α∞quickly
␈↓ α∧␈↓follows.

␈↓ α∧␈↓␈↓ αTSince␈αrecursive␈αdefinitions␈αgive␈αrise␈αto␈αpartial␈α
predicates,␈αand␈αwe␈αdon't␈αwant␈αto␈αuse␈αa␈α
partial
␈↓ α∧␈↓predicate␈α∞logic,␈α∞we␈α∞introduce␈α∞a␈α∞domain␈α∂␈↓	P␈↓␈α∞of␈α∞␈↓↓extended␈α∞truth␈α∞values␈↓␈α∞with␈α∂characteristic␈α∞predicate
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u6


␈↓ α∧␈↓␈↓↓isetv␈↓␈α
whose␈α
elements␈α
are␈α∞␈↓↓T,␈↓␈α
␈↓↓F␈↓␈α
and␈α
␈↓πT␈↓.␈α∞ There␈α
is␈α
no␈α
harm␈α
in␈α∞identifying␈α
␈↓↓T␈↓␈α
and␈α
␈↓↓F␈↓␈α∞with␈α
suitable
␈↓ α∧␈↓Lisp␈αatoms␈αor␈αwith␈αthe␈αintegers␈α1␈αand␈α0.␈α The␈αfollowing␈αaxioms␈αdescribe␈αfunctions␈αinto␈αor␈αout␈αof
␈↓ α∧␈↓␈↓	P␈↓.  We use the predicate ␈↓↓istv␈↓ to test for the honest truth values ␈↓↓T␈↓ and ␈↓↓F.␈↓

␈↓ α∧␈↓B0: ␈↓↓isetv ␈↓πT␈↓↓ ∧ istv T ∧ istv F␈↓

␈↓ α∧␈↓B1: ␈↓↓∀p.(isetv p)␈↓

␈↓ α∧␈↓B2: ␈↓↓∀p.(p = T ∨ p = F ∨ p = ␈↓πT␈↓↓)␈↓

␈↓ α∧␈↓B3: ␈↓↓T ≠ F ∧ T ≠ ␈↓πT␈↓↓ ∧ F ≠ ␈↓πT␈↓↓␈↓

␈↓ α∧␈↓B4: ␈↓↓∀p.(istv p ≡ p = T ∨ p = F)␈↓

␈↓ α∧␈↓B5: ␈↓↓∀p. isetv not p␈↓

␈↓ α∧␈↓B6: ␈↓↓∀p q. isetv(p and q)␈↓

␈↓ α∧␈↓B7: ␈↓↓∀p q. isetv(p or q)␈↓

␈↓ α∧␈↓B8: ␈↓↓∀p.(not p = ␈↓αif␈↓↓ (p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓

␈↓ α∧␈↓B9: ␈↓↓∀p q.(p and q = ␈↓αif␈↓↓ (p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓

␈↓ α∧␈↓B10: ␈↓↓∀p q.(p or q = (␈↓αif␈↓↓ p = ␈↓πT␈↓↓) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓

␈↓ α∧␈↓B11: ␈↓↓∀X Y.(X equal Y = ␈↓αif␈↓↓ ¬issexp X ∨ ¬issexp Y ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ X = Y ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓

␈↓ α∧␈↓B12: ␈↓↓∀X.(aatom X = ␈↓αif␈↓↓ ¬issexp X ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓t X ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓,

␈↓ α∧␈↓and we also need a conditional expression that can take an argument from ␈↓	P␈↓, namely

␈↓ α∧␈↓B13: ␈↓↓∀p X Y.(if(p,X,Y) = ␈↓αif␈↓↓ p = ␈↓πT␈↓↓ ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ X ␈↓αelse␈↓↓ Y)␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓occura␈↓␈αis␈αproved␈αtotal␈αby␈αapplying␈αschema␈αLS1␈αwith␈α␈↓↓␈↓	F␈↓↓(y)␈α≡␈αistv␈αoccura(x,y)␈α≠␈α␈↓πT␈↓↓␈↓.␈α After␈αthis
␈↓ α∧␈↓␈↓↓occur␈↓ can be shown to satisfy (10).

␈↓ α∧␈↓␈↓ αTThe␈α∂axioms␈α∂L1-L16␈α∂and␈α∂B1-B12␈α∂together␈α∂with␈α∂the␈α∂sentences␈α∂arising␈α∂from␈α∂the␈α∂schemata
␈↓ α∧␈↓LS1␈αand␈αLS2␈αwill␈αbe␈αcalled␈αthe␈αaxiom␈αsystem␈αLisp0.␈α We␈αwill␈αadjoin␈αone␈αmore␈αaxiom␈αlater␈αto␈αget
␈↓ α∧␈↓the system Lisp1.

␈↓ α∧␈↓␈↓ αTThe␈αabove␈α
method␈αof␈α
replacing␈αa␈α
recursion␈αby␈αa␈α
first␈αorder␈α
sentence␈αwas␈α
first␈α(I␈αthink)␈α
used
␈↓ α∧␈↓in (Cartwright 1977).  I'm surprised that it wasn't invented sooner.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u7


␈↓ α∧␈↓α5. An Extended Example.

␈↓ α∧␈↓␈↓ αTThe␈αSAMEFRINGE␈αproblem␈αis␈αto␈αwrite␈αa␈αprogram␈αthat␈αefficiently␈αdetermines␈αwhether␈αtwo
␈↓ α∧␈↓S-expressions␈α∞have␈α∞the␈α
same␈α∞fringe,␈α∞i.e.␈α
have␈α∞the␈α∞same␈α
atoms␈α∞in␈α∞the␈α
same␈α∞order.␈α∞ (Some␈α
people
␈↓ α∧␈↓omit␈αthe␈αNILs␈αat␈αthe␈αends␈αof␈αlists,␈αbut␈α
we␈αwill␈αtake␈αall␈αatoms).␈α Thus␈α((A.B).C)␈αand␈α(A.(B.C))␈α
have
␈↓ α∧␈↓the␈αsame␈αfringe,␈αnamely␈α(A␈αB␈αC).␈α The␈αobject␈αof␈αthe␈αoriginal␈αproblem␈αwas␈αto␈αprogram␈αit␈αusing␈αa
␈↓ α∧␈↓minimum␈α
of␈α
storage,␈αand␈α
it␈α
was␈αconjectured␈α
that␈α
co-routines␈αwere␈α
necessary␈α
to␈αdo␈α
it␈α
neatly.␈α We
␈↓ α∧␈↓shall not discuss that matter here - merely the extensional correctness of one proposed solution.

␈↓ α∧␈↓␈↓ αTThe relevant recursive definitions are

␈↓ α∧␈↓13)␈↓ αt ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ α∧␈↓where ␈↓↓u * v␈↓ denotes the result of appending the lists ␈↓↓u␈↓ and ␈↓↓v␈↓ and is defined recursively by

␈↓ α∧␈↓14)␈↓ αt ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ α∧␈↓We are interested in the condition ␈↓↓fringe x = fringe y␈↓.

␈↓ α∧␈↓␈↓ αTThe function to be proved correct is ␈↓↓samefringe[x,y]␈↓ defined by the simultaneous recursion

␈↓ α∧␈↓15)␈↓ αt ␈↓↓samefringe[x, y] ← (x = y) ∨ [¬␈↓αa␈↓↓t x ∧ ¬␈↓αa␈↓↓t y ∧ same[gopher x, gopher y]]␈↓,

␈↓ α∧␈↓16)␈↓ αt ␈↓↓same[x, y] ← (␈↓αa␈↓↓ x = ␈↓αa␈↓↓ y) ∧ samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ α∧␈↓where

␈↓ α∧␈↓17)␈↓ αt ␈↓↓gopher x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]␈↓.

␈↓ α∧␈↓␈↓ αTWe need to prove that ␈↓↓samefringe␈↓ is total and

␈↓ α∧␈↓18)␈↓ αt ␈↓↓∀xy.(samefringe[x,y] ≡ fringe x = fringe y)␈↓.

␈↓ α∧␈↓␈↓ αTThe␈αminimization␈α
schemata␈αof␈α
these␈αfunctions␈α
are␈αirrelevant,␈α
because␈αwe␈α
will␈αprove␈αthat␈α
the
␈↓ α∧␈↓functions␈αare␈αall␈αtotal␈αexcept␈αthat␈αwe␈αwon't␈αprove␈αanything␈αabout␈αthe␈αresult␈αof␈αapplying␈α␈↓↓gopher␈↓␈αto
␈↓ α∧␈↓an atom.  The functional equations are

␈↓ α∧␈↓19)␈↓ αt ␈↓↓∀x.(fringe x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓),

␈↓ α∧␈↓20)␈↓ αt ␈↓↓∀u v.(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓.

␈↓ α∧␈↓21)␈↓ αt␈α
␈↓↓∀x␈αy.(samefringe[x,␈α
y]␈α
=␈αx␈α
equal␈α
y␈αor␈α
[not␈αaat␈α
x␈α
and␈αnot␈α
aat␈α
y␈αand␈α
same[gopher␈αx,␈α
gopher
␈↓ α∧␈↓↓y]])␈↓,

␈↓ α∧␈↓22)␈↓ αt ␈↓↓∀x y.(same[x, y] = ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ α∧␈↓23)␈↓ αt ␈↓↓∀x.(gopher x = ␈↓αif␈↓↓ ␈↓αa␈↓↓t ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x])␈↓.

␈↓ α∧␈↓Note␈α∞that␈α
because␈α∞␈↓↓samefringe␈↓␈α
and␈α∞␈↓↓same␈↓␈α
are␈α∞recursively␈α
defined␈α∞predicates␈α
which␈α∞have␈α∞not␈α
been
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u8


␈↓ α∧␈↓proved␈α
total,␈α
their␈α
functional␈α
equations␈α
must␈α
use␈α
the␈α
imitation␈α
propositional␈α∞functions␈α
involving
␈↓ α∧␈↓the extended truth values.

␈↓ α∧␈↓␈↓ αTWe␈αshall␈αnot␈α
give␈αfull␈αproofs␈αbut␈α
merely␈αthe␈αinduction␈αpredicates␈α
and␈αa␈αfew␈α
indications␈αof
␈↓ α∧␈↓the algebraic transformations.  We begin with a lemma about ␈↓↓gopher␈↓.

␈↓ α∧␈↓24)␈↓ αt ␈↓↓∀x y.(issexp gopher[x.y] ∧ ␈↓αa␈↓↓t ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ α∧␈↓␈↓ αTThis lemma can be proved by S-expression structural induction using the predicate

␈↓ α∧␈↓25)␈↓ αt ␈↓↓P(x) ≡ ∀y.ok(x,y)␈↓,

␈↓ α∧␈↓where ␈↓↓ok(x,y)␈↓ is defined by

␈↓ α∧␈↓26)␈↓ αt␈↓↓∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ ␈↓αa␈↓↓t ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ α∧␈↓In␈α#the␈α#course␈α"of␈α#the␈α#proof,␈α#we␈α"use␈α#the␈α#associativity␈α"of␈α#*␈α#and␈α#the␈α"formula
␈↓ α∧␈↓␈↓↓fringe[x.y] = fringe x * fringe y␈↓.␈α
 The␈α
lemma␈α
was␈α
expressed␈α
using␈α
␈↓↓gopher[x.y]␈↓␈α
in␈α
order␈α∞to␈α
avoid
␈↓ α∧␈↓considering␈α
atomic␈αarguments␈α
for␈α␈↓↓gopher␈↓,␈α
but␈αit␈α
could␈α
have␈αequally␈α
well␈αbe␈α
proved␈αabout␈α
␈↓↓gopher x␈↓
␈↓ α∧␈↓with the condition ␈↓↓¬␈↓αa␈↓↓t x␈↓.

␈↓ α∧␈↓␈↓ αTAnother␈αproof␈αcan␈αbe␈αgiven␈αusing␈αthe␈αcourse-of-values␈αinduction␈αschema␈αfor␈αintegers.␈α We
␈↓ α∧␈↓write this schema

␈↓ α∧␈↓ICV: ␈↓↓∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)␈↓,

␈↓ α∧␈↓where␈α␈↓↓m␈↓␈αand␈α␈↓↓n␈↓␈α
range␈αover␈αnon-negative␈αintegers.␈α
 Exactly␈αthe␈αsame␈αschema␈α
expresses␈αtransfinite
␈↓ α∧␈↓induction;␈αwe␈α
need␈αonly␈α
imagine␈αthe␈αvariables␈α
ranging␈αover␈α
all␈αordinals␈αless␈α
than␈αa␈α
given␈αone␈α-␈α
in
␈↓ α∧␈↓this case ␈↓	w␈↓, but equally well ␈↓	w␈↓#
w␈↓#␈↓ or ε␈↓β0␈↓.  We also use the function ␈↓↓size x␈↓ defined by

␈↓ α∧␈↓27)␈↓ αt ␈↓↓size x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ size ␈↓αa␈↓↓ x + size ␈↓αd␈↓↓ x␈↓

␈↓ α∧␈↓satisfying the obvious functional equation.  Our induction predicate is then

␈↓ α∧␈↓28)␈↓ αt ␈↓↓P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))␈↓.

␈↓ α∧␈↓␈↓ αTFor our proof about ␈↓↓samefringe␈↓ we need one more lemma about ␈↓↓gopher␈↓, namely

␈↓ α∧␈↓29)␈↓ αt ␈↓↓∀x y.(size gopher[x.y] = size[x.y]␈↓.

␈↓ α∧␈↓␈↓ αTThis␈α→can␈α_be␈α→proved␈α→by␈α_either␈α→of␈α_the␈α→above␈α→inductive␈α_methods␈α→or␈α→by␈α_including
␈↓ α∧␈↓␈↓↓size gopher[x.y] = size[x.y]␈↓ in the induction hypothesis ␈↓↓ok[x,y]␈↓.

␈↓ α∧␈↓␈↓ αTThe statement about samefringe is

␈↓ α∧␈↓30)␈↓ αt ␈↓↓∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x = fringe y)␈↓,

␈↓ α∧␈↓and it is most easily proved by induction on ␈↓↓size x + size y␈↓ using the predicate
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ u9


␈↓ α∧␈↓31)␈↓ αt␈α␈↓↓P(n)␈α≡␈α
∀x␈αy.(n␈α=␈α
size␈αx␈α+␈α
size␈αy␈α⊃␈α
issexp␈αsamefringe[x,y]␈α∧␈α
(samefringe[x,y]␈α=␈αT␈α≡␈α
fringe
␈↓ α∧␈↓↓x = fringe y))␈↓.

␈↓ α∧␈↓It␈α
can␈αalso␈α
be␈αproved␈α
using␈α
the␈αwell-foundedness␈α
of␈αlexicographic␈α
ordering␈α
of␈αthe␈α
list␈α␈↓↓<x␈α
␈↓αa␈↓↓␈αx>␈↓,␈α
but
␈↓ α∧␈↓then we must decide what lexicographic orderings to include in our axiom system.

␈↓ α∧␈↓␈↓ αTTransfinite␈α
induction␈α
is␈α∞also␈α
useful,␈α
and␈α∞can␈α
be␈α
illustrated␈α∞with␈α
a␈α
variant␈α∞␈↓↓samefringe␈↓␈α
that
␈↓ α∧␈↓does everything in one complicated recursive definition, namely

␈↓ α∧␈↓32)␈↓ αt␈α␈↓↓samefringe[x,y]␈α=␈α(x␈αequal␈αy)␈αor␈αnot␈αaat␈αx␈αand␈α
not␈αaat␈αy␈αand␈α[␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈α␈↓αa␈↓↓␈αx␈α␈↓αthen␈↓↓␈α[␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈αy␈α
␈↓αthen␈↓↓
␈↓ α∧␈↓↓␈↓αa␈↓↓␈α
x␈α
equal␈α
␈↓αa␈↓↓␈α
y␈α
and␈α
samefringe[␈↓αd␈↓↓␈α
x,␈α
␈↓αd␈↓↓␈α
y]␈α
␈↓αelse␈↓↓␈α
samefringe[x,␈α
␈↓αaa␈↓↓␈α
y␈α
.␈α
[␈↓αda␈↓↓␈α
y␈α
.␈α
␈↓αd␈↓↓␈α
y]]]␈α
␈↓αelse␈↓↓␈αsamefringe[␈↓αaa␈↓↓␈α
x
␈↓ α∧␈↓↓. [␈↓αda␈↓↓ x .␈↓αd␈↓↓ x], y]␈↓.

␈↓ α∧␈↓The transfinite induction predicate then has the form

␈↓ α∧␈↓33)␈↓ αt␈α∞␈↓↓P(n)␈α∂≡␈α∞∀x␈α∞y.[n␈α∂=␈α∞␈↓	w␈↓↓(size␈α∞x␈α∂+␈α∞size␈α∂y)␈α∞+␈α∞size␈α∂␈↓αa␈↓↓␈α∞x␈α∞+␈α∂size␈α∞␈↓αa␈↓↓␈α∞y␈α∂⊃␈α∞issexp␈α∂samefringe[x,y]␈α∞∧
␈↓ α∧␈↓↓(samefringe[x,y] = T ≡ fringe x = fringe y)]␈↓.

␈↓ α∧␈↓␈↓ αTAn␈α
easier␈αexample␈α
requiring␈α
induction␈αup␈α
to␈α␈↓	w␈↓∧2␈↓␈α
is␈α
proving␈αthe␈α
termination␈αof␈α
Ackermann's
␈↓ α∧␈↓function which has the functional equation

␈↓ α∧␈↓2034)␈↓ αt ␈↓↓∀m n.(A(m,n) = ␈↓αif␈↓↓ m = 0 ␈↓αthen␈↓↓ n+1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ A(m-1,0) ␈↓αelse␈↓↓ A(m-1,A(m,n-1)))␈↓.

␈↓ α∧␈↓The statement to be proved is

␈↓ α∧␈↓2035)␈↓ αt ␈↓↓∀.( < ␈↓	w␈↓∧2␈↓↓ ∧  = ␈↓	w␈↓↓m + n ⊃ isint A(m,n))␈↓.

␈↓ α∧␈↓The␈α
proof␈α
is␈αstraightforward,␈α
because␈α
␈↓	w␈↓↓(m-1) < ␈↓	w␈↓↓m+n␈↓␈α
and␈α␈↓	w␈↓↓m+(n-1) < ␈↓	w␈↓↓m+n␈↓,␈α
so␈α
we␈αcan␈α
assume
␈↓ α∧␈↓␈↓↓isint A(m-1,0)␈↓␈α∞and␈α∂␈↓↓isint A(m,n-1)␈↓.␈α∞ From␈α∞the␈α∂latter,␈α∞it␈α∞follows␈α∂that␈α∞␈↓	w␈↓↓(m-1)+A(m,n-1) < ␈↓	w␈↓↓m+n␈↓
␈↓ α∧␈↓which completes the induction step.

␈↓ α∧␈↓␈↓ αTWe␈α↔would␈α↔like␈α↔to␈α↔prove␈α↔that␈α↔the␈α↔amount␈α↔of␈α↔storage␈α↔used␈α↔in␈α↔the␈α↔computation␈α⊗of
␈↓ α∧␈↓␈↓↓samefringe[x,y]␈↓␈αaside␈α
from␈αthat␈αoccupied␈α
by␈α␈↓↓x␈↓␈α
and␈α␈↓↓y,␈↓␈αnever␈α
exceeds␈αthe␈αsum␈α
of␈αthe␈α
numbers␈αof
␈↓ α∧␈↓␈↓↓car␈↓s␈αrequired␈αto␈αreach␈αcorresponding␈αatoms␈αin␈α␈↓↓x␈↓␈αand␈α␈↓↓y.␈↓␈αUnfortunately,␈αwe␈αcan't␈αeven␈αexpress␈αthat
␈↓ α∧␈↓fact,␈αbecause␈αwe␈α
are␈αaxiomatizing␈αthe␈αprograms␈α
as␈αfunctions,␈αand␈αthe␈α
amount␈αof␈αstorage␈αused␈α
does
␈↓ α∧␈↓not␈α∞depend␈α∞merely␈α∞on␈α∂the␈α∞function␈α∞being␈α∞computed;␈α∞it␈α∂depends␈α∞on␈α∞the␈α∞method␈α∂of␈α∞computation.
␈↓ α∧␈↓We␈αmay␈α
regard␈αsuch␈αthings␈α
as␈α␈↓↓intensional␈↓␈αproperties,␈α
but␈αany␈αcorrespondence␈α
with␈αthe␈α
notion␈αof
␈↓ α∧␈↓intensional properties in intensional logic remains to be established.


␈↓ α∧␈↓α6. The Minimization Schema.

␈↓ α∧␈↓␈↓ αTThe␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ α∧␈↓program

␈↓ α∧␈↓36)␈↓ αt ␈↓↓f1 x ← f1 x␈↓

␈↓ α∧␈↓leads to the sentence

␈↓ α∧␈↓37)␈↓ αt ␈↓↓∀x.(f1 x = f1 x)␈↓
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f10


␈↓ α∧␈↓which␈αprovides␈αno␈αinformation␈αalthough␈αthe␈αfunction␈α␈↓↓f␈↓␈αis␈αundefined␈αfor␈αall␈α␈↓↓x.␈↓␈αThis␈αis␈αnot␈αalways
␈↓ α∧␈↓the case, since the program

␈↓ α∧␈↓38)␈↓ αt ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓

␈↓ α∧␈↓has the functional equation

␈↓ α∧␈↓39)␈↓ αt ␈↓↓∀x.(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.

␈↓ α∧␈↓from which ␈↓↓∀x.¬issexp f2(x)␈↓ can be proved by induction.

␈↓ α∧␈↓␈↓ αTIn␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ α∧␈↓defined solution of the functional equation.

␈↓ α∧␈↓␈↓ αTSuppose the program is

␈↓ α∧␈↓40)␈↓ αt ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ α∧␈↓yielding the functional equation

␈↓ α∧␈↓41)␈↓ αt ␈↓↓∀x.(f x = ␈↓	t␈↓↓[f](x)␈↓.

␈↓ α∧␈↓The ␈↓↓minimization schema␈↓ is then

␈↓ α∧␈↓42)␈↓ αt ␈↓↓∀x.(isD ␈↓	t␈↓↓[␈↓	f␈↓↓](x) ⊃ ␈↓	f␈↓↓ x = ␈↓	t␈↓↓[␈↓	f␈↓↓](x)) ⊃ ∀x.(isD f x ⊃ ␈↓	f␈↓↓ x = f x)␈↓,

␈↓ α∧␈↓where the predicate ␈↓↓isD␈↓ asserts that its argument is in the domain ␈↓↓D␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α∞␈↓↓minimization␈α
schema␈↓␈α∞can␈α
be␈α∞abbreviated␈α
by␈α∞introducing␈α
Scott's␈α∞partial␈α
ordering␈α∞␈↓πb␈↓␈α
on
␈↓ α∧␈↓D␈↓∧+␈↓.  We define

␈↓ α∧␈↓43)␈↓ αt␈↓↓∀X Y.(X ␈↓πb␈↓↓ Y ≡ X = ␈↓πT␈↓↓ ∨ X = Y)␈↓,

␈↓ α∧␈↓so␈αthat␈αthe␈αonly␈αproper␈αordering␈αis␈αthat␈α␈↓πT␈↓␈αis␈αless␈αthan␈αeverything␈αelse.␈α We␈αalso␈αuse␈αthe␈αsymbol␈α␈↓πd␈↓.
␈↓ α∧␈↓The minimization schema then becomes

␈↓ α∧␈↓44)␈↓ αt ␈↓↓∀x.(␈↓	t␈↓↓[␈↓	f␈↓↓](x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x)) ⊃ ∀x.(f(x) ␈↓πb␈↓↓ ␈↓	f␈↓↓(x))␈↓,

␈↓ α∧␈↓which makes it more apparent that the minimization schema asserts that ␈↓↓f␈↓ is minimal.

␈↓ α∧␈↓␈↓ αTIn the ␈↓↓subst␈↓ example, the schema is

␈↓ α∧␈↓45)␈↓ αt␈↓↓∀x␈αy␈α
z.(␈↓	f␈↓↓(x,y,z)␈α␈↓πd␈↓↓␈α
␈↓αif␈↓↓␈α␈↓αa␈↓↓t␈α
z␈α␈↓αthen␈↓↓␈α
(␈↓αif␈↓↓␈αz␈α=␈α
y␈α␈↓αthen␈↓↓␈α
x␈α␈↓αelse␈↓↓␈α
z)␈α␈↓αelse␈↓↓␈α
␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈αz).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α
z))␈α⊃␈α∀x␈α
y
␈↓ α∧␈↓↓z.(␈↓	f␈↓↓(x,y,z) ␈↓πd␈↓↓ subst(x,y,z))␈↓,

␈↓ α∧␈↓which has also the longer form

␈↓ α∧␈↓46)␈↓ αt␈α⊂␈↓↓∀x␈α⊂y␈α⊂z.(issexp␈α⊂(␈↓αif␈↓↓␈α⊂␈↓αa␈↓↓t␈α⊂z␈α⊂␈↓αthen␈↓↓␈α⊂(␈↓αif␈↓↓␈α⊂z␈α⊂=␈α⊂y␈α⊂␈↓αthen␈↓↓␈α⊂x␈α⊂␈↓αelse␈↓↓␈α⊂z)␈α⊂␈↓αelse␈↓↓␈α⊂␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α⊂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α⊂z))␈α⊂⊃
␈↓ α∧␈↓↓(␈↓	f␈↓↓(x,y,z)␈α∞=␈α∞␈↓αif␈↓↓␈α∞␈↓αa␈↓↓t␈α∞z␈α∞␈↓αthen␈↓↓␈α∞(␈↓αif␈↓↓␈α∞z␈α∞=␈α∞y␈α∞␈↓αthen␈↓↓␈α∞x␈α∞␈↓αelse␈↓↓␈α∞z)␈α∞␈↓αelse␈↓↓␈α∞␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α∞z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α∞z)))␈α∞⊃␈α∞∀x␈α∞y␈α∞z.(issexp
␈↓ α∧␈↓↓subst(x,y,z) ⊃ ␈↓	f␈↓↓(x,y,z) = subst(x,y,z))␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f11


␈↓ α∧␈↓␈↓ αTIn␈αthe␈αschema␈α␈↓	f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ α∧␈↓schema is just a translation into first order logic of Park's (1970) theorem

␈↓ α∧␈↓47)␈↓ αt ␈↓↓␈↓	f␈↓↓ ␈↓πd␈↓↓ ␈↓	t␈↓↓[␈↓	f␈↓↓] ⊃ ␈↓	f␈↓↓ ␈↓πd␈↓↓ Y[␈↓	t␈↓↓]␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(36)␈α
is␈α
never␈αan␈α
S-
␈↓ α∧␈↓expression.  The schema becomes

␈↓ α∧␈↓48)␈↓ αt ␈↓↓∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ ␈↓	f␈↓↓ x) ⊃ ∀x.(␈↓	f␈↓↓ x ␈↓πd␈↓↓ f1 x)␈↓,

␈↓ α∧␈↓and we take

␈↓ α∧␈↓49)␈↓ αt ␈↓↓␈↓	f␈↓↓ x = ␈↓πT␈↓↓␈↓.

␈↓ α∧␈↓The␈αleft␈αside␈αof␈α(48)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓πT␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ α∧␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.

␈↓ α∧␈↓␈↓ αTThe␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ α∧␈↓the well known 91-function is defined by the recursive program over the integers

␈↓ α∧␈↓50)␈↓ αt ␈↓↓f91 x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.

␈↓ α∧␈↓The goal is to show that

␈↓ α∧␈↓51)␈↓ αt ␈↓↓∀x.(f91 x = ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91)␈↓.

␈↓ α∧␈↓We apply the minimization schema with

␈↓ α∧␈↓52)␈↓ αt ␈↓↓␈↓	f␈↓↓ x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,

␈↓ α∧␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ α∧␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.

␈↓ α∧␈↓␈↓ αTThe␈α
method␈α
of␈α
recursion␈α
induction␈α
(McCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ α∧␈↓minimization␈α
schema.␈α
 If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ α∧␈↓we␈α
show␈α
that␈αthey␈α
both␈α
equal␈α
the␈αfunction␈α
computed␈α
by␈α
the␈αprogram␈α
on␈α
whereever␈α
the␈αfunction␈α
is
␈↓ α∧␈↓defined.

␈↓ α∧␈↓␈↓ αTThe␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ α∧␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ α∧␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ α∧␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ α∧␈↓higher order logic, will improve our ability to use the schema in proofs.

␈↓ α∧␈↓␈↓ αT(42)␈α∞can␈α∞be␈α∂regarded␈α∞as␈α∞an␈α∂axiom␈α∞schema␈α∞involving␈α∞a␈α∂second␈α∞order␈α∞function␈α∂variable␈α∞␈↓	t␈↓.
␈↓ α∧␈↓What␈αcan␈αbe␈αsubstituted␈αfor␈α␈↓	t␈↓␈αis␈αa␈αquantifier␈αfree␈αλ-expression␈αin␈αa␈αfirst␈αorder␈αfunction␈αvariable.
␈↓ α∧␈↓It␈α
may␈α
be␈α
interesting␈α
to␈α
study␈α
the␈α
sets␈α
of␈α
first␈α
order␈α
sentences␈α
that␈α
can␈α
be␈α
generated␈α
by␈αsuch␈α
second
␈↓ α∧␈↓order␈αsentence␈αschemata.␈α Presumably,␈αsets␈αof␈αsentences␈αcan␈αbe␈αgenerated␈αin␈αthis␈αway␈αthat␈αcannnot
␈↓ α∧␈↓be generated by schemata with only first order function variables.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f12


␈↓ α∧␈↓α7. Proof Methods as Axiom Schemata

␈↓ α∧␈↓␈↓ αTRepresenting␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ α∧␈↓methods for proving partial correctness as axiom schemata of first order logic.

␈↓ α∧␈↓␈↓ αTFor example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by

␈↓ α∧␈↓53)␈↓ αt ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓

␈↓ α∧␈↓satisfies␈α␈↓↓␈↓	F␈↓↓(x)␈↓,␈αthen␈αif␈αthe␈αfunction␈αterminates,␈αthe␈αoutput␈α␈↓↓f(x)␈↓␈αwill␈αsatisfy␈α␈↓	Y␈↓↓(x,f(x))␈↓.␈α We␈αappeal␈αto
␈↓ α∧␈↓the following ␈↓↓axiom schema of inductive assertions␈↓:

␈↓ α∧␈↓54)␈↓ αt ␈↓↓∀x.(␈↓	F␈↓↓(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓	Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ α∧␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD f x ⊃ ␈↓	Y␈↓↓(x,f x))␈↓


␈↓ α∧␈↓where␈α␈↓↓isD␈α
f␈αx␈↓␈α
is␈αthe␈α
assertion␈αthat␈α
␈↓↓f(x)␈↓␈αis␈α
in␈αthe␈α
nominal␈αrange␈α
of␈αthe␈α
function␈αdefinition,␈α
i.e.␈αis␈α
an
␈↓ α∧␈↓integer␈α∞or␈α
an␈α∞S-expression␈α∞as␈α
the␈α∞case␈α
may␈α∞be,␈α∞and␈α
asserts␈α∞that␈α
the␈α∞computation␈α∞terminates.␈α
 In
␈↓ α∧␈↓order␈α⊂to␈α⊂use␈α⊂the␈α∂schema,␈α⊂we␈α⊂must␈α⊂invent␈α∂a␈α⊂suitable␈α⊂predicate␈α⊂␈↓↓q(x,y)␈↓,␈α∂and␈α⊂this␈α⊂is␈α⊂precisely␈α∂the
␈↓ α∧␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓	F␈↓,␈α␈↓	Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ α∧␈↓schema can be written for any collection of mutually recursive definitions that is iterative.

␈↓ α∧␈↓␈↓ αTThe␈α∂method␈α∂of␈α∞␈↓↓subgoal␈α∂induction␈↓␈α∂for␈α∞recursive␈α∂programs␈α∂was␈α∞introduced␈α∂in␈α∂(Manna␈α∞and
␈↓ α∧␈↓Pnueli␈α∂1970),␈α⊂but␈α∂they␈α∂didn't␈α⊂give␈α∂it␈α⊂a␈α∂name.␈α∂ Morris␈α⊂and␈α∂Wegbreit␈α∂(1977)␈α⊂name␈α∂it,␈α⊂extend␈α∂it
␈↓ α∧␈↓somewhat,␈α⊂and␈α⊂apply␈α⊂it␈α∂to␈α⊂Algol-like␈α⊂programs.␈α⊂ Unlike␈α∂␈↓↓inductive␈α⊂assertions␈↓,␈α⊂it␈α⊂isn't␈α⊂limited␈α∂to
␈↓ α∧␈↓iterative definitions.  Thus, for the recursive program

␈↓ α∧␈↓55)␈↓ αt ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,

␈↓ α∧␈↓where ␈↓↓p␈↓ is assumed total, we have

␈↓ α∧␈↓56)␈↓ αt ␈↓↓∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ ∀x.(␈↓	F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓	Y␈↓↓(x,z))
␈↓ α∧␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD(f(x)) ⊃ ␈↓	Y␈↓↓(x,f(x)))␈↓

␈↓ α∧␈↓␈↓ αTWe␈α∞can␈α∞express␈α∞these␈α∞methods␈α∞as␈α∂axiom␈α∞schemata,␈α∞because␈α∞we␈α∞have␈α∞the␈α∞predicate␈α∂␈↓↓isD␈↓␈α∞to
␈↓ α∧␈↓express␈α∞termination.␈α∞ The␈α∞minimization␈α∞schema␈α∞itself␈α∞can␈α∞be␈α∞proved␈α∞by␈α∞subgoal␈α∞induction.␈α
 We
␈↓ α∧␈↓need only take ␈↓↓␈↓	F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓	Y␈↓↓(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓ and ␈↓↓q(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓.

␈↓ α∧␈↓␈↓ αTGeneral␈α
rules␈αfor␈α
going␈αfrom␈α
a␈αrecursive␈α
program␈α
to␈αwhat␈α
amounts␈αto␈α
the␈αsubgoal␈α
induction
␈↓ α∧␈↓schema␈α
are␈α
given␈α
in␈α
(Manna␈α
and␈α
Pnueli␈α
1970)␈α
and␈α
(Morris␈α
and␈α
Wegbreit␈α
1977);␈α
we␈α
need␈α
only␈α
add
␈↓ α∧␈↓a conclusion involving the ␈↓↓isD␈↓ predicate to the Manna's and Pnueli formula ␈↓↓W␈↓βP␈↓.

␈↓ α∧␈↓␈↓ αTHowever,␈α∞we␈α
can␈α∞characterize␈α
subgoal␈α∞induction␈α
as␈α∞an␈α
axiom␈α∞schema.␈α
 Namely,␈α∞we␈α
define
␈↓ α∧␈↓␈↓	t␈↓↓'[q]␈↓ as an extension of ␈↓	t␈↓ mapping relations into relations.  Thus if

␈↓ α∧␈↓57)␈↓ αt ␈↓↓␈↓	t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f g2 x␈↓,

␈↓ α∧␈↓we have

␈↓ α∧␈↓58)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ (y = h x) ␈↓αelse␈↓↓ ∃z.(q(g2 x,z) ∧ y = g1 z)␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f13


␈↓ α∧␈↓In general we have

␈↓ α∧␈↓59)␈↓ αt ␈↓↓∀xy.(␈↓	t␈↓↓'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))␈↓,

␈↓ α∧␈↓from␈α
which␈α
the␈α
subgoal␈α
induction␈α
rule␈α
follows␈α∞immediately␈α
given␈α
the␈α
properties␈α
of␈α
␈↓	F␈↓␈α
and␈α∞␈↓	Y␈↓.␈α
 I
␈↓ α∧␈↓am indebted to Wolfgang Polak (oral communication) for help in elucidating this relationship.

␈↓ α∧␈↓␈↓αWARNING␈↓:␈αThe␈αrest␈α
of␈αthis␈αsection␈α
is␈αstill␈αsomewhat␈α
conjectural␈αand␈αis␈α
subject␈αto␈αchange.␈α
 There
␈↓ α∧␈↓may be bugs.

␈↓ α∧␈↓␈↓ αTThe␈αextension␈α␈↓↓␈↓	t␈↓↓'[q]␈↓␈α
can␈αbe␈αdetermined␈αas␈α
follows:␈αIntroduce␈αinto␈αthe␈α
logic␈αthe␈αnotion␈α
of␈αa
␈↓ α∧␈↓␈↓↓multi-term␈↓␈α
which␈αis␈α
formed␈αin␈α
the␈αsame␈α
way␈α
as␈αa␈α
term␈αbut␈α
allows␈αrelations␈α
written␈α
as␈αfunctions.
␈↓ α∧␈↓For␈α∀the␈α∀present␈α∃we␈α∀won't␈α∀interpret␈α∃them␈α∀but␈α∀merely␈α∀give␈α∃rules␈α∀for␈α∀introducing␈α∃them␈α∀and
␈↓ α∧␈↓subsequently␈α
eliminating␈αthem␈α
again␈α
to␈αget␈α
an␈α
ordinary␈αformula.␈α
 Thus␈α
we␈αwill␈α
write␈α
␈↓↓q<e>␈↓␈αwhere␈α
␈↓↓e␈↓
␈↓ α∧␈↓is␈αany␈αterm␈αor␈αmulti-term.␈α We␈αthen␈αform␈α␈↓↓␈↓	t␈↓↓'[q]␈↓␈αexactly␈αin␈αthe␈αsame␈αway␈α␈↓↓␈↓	t␈↓↓[f]␈↓␈αwas␈αformed.␈α Thus
␈↓ α∧␈↓for the 91-function we have

␈↓ α∧␈↓60)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x) = ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>␈↓.

␈↓ α∧␈↓The␈α⊃pointy␈α⊃brackets␈α⊂indicate␈α⊃that␈α⊃we␈α⊂are␈α⊃"applying"␈α⊃a␈α⊂relation.␈α⊃ We␈α⊃now␈α⊃evaluate␈α⊂␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓
␈↓ α∧␈↓formally as follows:

␈↓ α∧␈↓61)␈↓ αt ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ (␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>)(y)

␈↓ α∧␈↓↓≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ q(q<x+11>,y)

␈↓ α∧␈↓↓≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ ∃z.(q(x+11,z) ∧ q(z,y))␈↓.

␈↓ α∧␈↓This␈α⊂last␈α⊂formula␈α∂has␈α⊂no␈α⊂pointy␈α∂brackets␈α⊂and␈α⊂is␈α∂just␈α⊂the␈α⊂formula␈α∂that␈α⊂would␈α⊂be␈α⊂obtained␈α∂by
␈↓ α∧␈↓Manna and Pnueli or Morris and Wegbreit.  The rules are as follows:

␈↓ α∧␈↓␈↓ αT(i)␈α∂␈↓↓␈↓	t␈↓↓'[q](x)␈↓␈α∞is␈α∂just␈α∞like␈α∂␈↓↓␈↓	t␈↓↓[f](x)␈↓␈α∞except␈α∂that␈α∂␈↓↓q␈↓␈α∞replaces␈α∂␈↓↓f␈↓␈α∞and␈α∂takes␈α∞its␈α∂arguments␈α∂in␈α∞pointy
␈↓ α∧␈↓brackets.

␈↓ α∧␈↓␈↓ αT(ii) an ordinary term ␈↓↓e␈↓ applied to ␈↓↓y␈↓ becomes ␈↓↓y = e␈↓.

␈↓ α∧␈↓␈↓ αT(ii) ␈↓↓q<e>(y)␈↓ becomes ␈↓↓q(e,y)␈↓.

␈↓ α∧␈↓␈↓ αT(ii)␈α∪␈↓↓P(q<e>)␈↓␈α∩becomes␈α∪␈↓↓∃z.q(e,z) ∧ P(z)␈↓␈α∩when␈α∪␈↓↓P(q<e>)␈↓␈α∩occurs␈α∪positively␈α∩in␈α∪␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓␈α∩and
␈↓ α∧␈↓becomes␈α⊂␈↓↓∀z.q(e,z) ⊃ P(z)␈↓␈α⊂when␈α⊂the␈α⊂occurrence␈α⊂is␈α⊂negatve.␈α⊂ It␈α⊂is␈α⊂not␈α⊂evident␈α⊃what␈α⊂independent
␈↓ α∧␈↓semantics should be given to multi-terms.




␈↓ α∧␈↓α8. Representations Using Finite Approximations.

␈↓ α∧␈↓␈↓ αTOur␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ α∧␈↓to␈α⊂G␈↓
:␈↓odel␈α⊂(1931,␈α∂1934)␈α⊂who␈α⊂showed␈α∂that␈α⊂primitive␈α⊂recursive␈α∂functions␈α⊂could␈α⊂be␈α⊂so␈α∂represented.
␈↓ α∧␈↓(Our knowledge of G␈↓
:␈↓odel's work comes from (Kleene 1951)).
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f14


␈↓ α∧␈↓␈↓ αTKleene␈α(1951)␈α
calls␈αa␈αfunction␈α
␈↓↓f␈↓␈α␈↓↓representable␈↓␈αif␈α
there␈αis␈αan␈α
arithmetic␈αformula␈α␈↓↓A␈↓␈α
with␈αfree
␈↓ α∧␈↓variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that

␈↓ α∧␈↓1)␈↓ αt ␈↓↓∀x y.((y = f(x)) ≡ A)␈↓,

␈↓ α∧␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ α∧␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ α∧␈↓representable.␈α The␈α
proof␈αinvolves␈αG␈↓
:␈↓odel␈α
numbering␈αpossible␈α
computation␈αsequences␈αand␈α
showing
␈↓ α∧␈↓that␈α
the␈α∞relation␈α
between␈α
sequences␈α∞and␈α
their␈α
elements␈α∞and␈α
the␈α
steps␈α∞of␈α
the␈α
computation␈α∞are␈α
all
␈↓ α∧␈↓representable.

␈↓ α∧␈↓␈↓ αTIn␈αLisp␈αless␈αmachinery␈α
is␈αneeded,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈αrelation␈α
between
␈↓ α∧␈↓a␈αsequence␈αand␈αits␈αelements␈αis␈αgiven␈αby␈αbasic␈αLisp␈αfunctions␈αand␈αby␈αthe␈α␈↓↓occurence␈αrelation␈↓␈αdefined
␈↓ α∧␈↓in section 5 by

␈↓ α∧␈↓2)␈↓ αt ␈↓↓occur[x,y] ← (x = y) ∨ ¬␈↓αa␈↓↓t y ∧ [occur[x,␈↓αa␈↓↓ y] ∨ occur[x, ␈↓αd␈↓↓ y]]␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓occur␈↓␈α∂is␈α∞the␈α∂only␈α∞recursive␈α∂definition␈α∞we␈α∂shall␈α∂require.␈α∞ Since␈α∂it␈α∞is␈α∂total,␈α∞we␈α∂only␈α∂need␈α∞its
␈↓ α∧␈↓functional equation to represent it in first order logic.  The functional equation is

␈↓ α∧␈↓L17: ␈↓↓∀x y.(occur[x,y] ≡ (x=y) ∨ ¬␈↓αa␈↓↓t y ∧ (occur[x,␈↓αa␈↓↓ y] ∨ occur[x,␈↓αd␈↓↓ y]))␈↓,

␈↓ α∧␈↓␈↓ αTThe␈α⊃axiom␈α⊃system␈α⊃consisting␈α⊂of␈α⊃L1-L17,␈α⊃B1-B12,␈α⊃and␈α⊂the␈α⊃sentences␈α⊃resulting␈α⊃from␈α⊂the
␈↓ α∧␈↓schemata LS1 and LS2 will be called the axiom system Lisp1.

␈↓ α∧␈↓␈↓ αTStarting␈α
with␈α
␈↓↓occur␈↓␈α
and␈α
the␈α
basic␈α
Lisp␈αfunctions␈α
and␈α
predicates␈α
we␈α
will␈α
define␈α
three␈αother
␈↓ α∧␈↓Lisp␈α⊃predicates␈α⊂without␈α⊃recursion.␈α⊂ By␈α⊃␈↓↓u istail v␈↓␈α⊂we␈α⊃mean␈α⊂that␈α⊃␈↓↓u␈↓␈α⊂can␈α⊃be␈α⊂obtained␈α⊃from␈α⊃␈↓↓v␈↓␈α⊂by
␈↓ α∧␈↓repeated␈α␈↓↓cdr␈↓s.␈α Thus␈αthe␈αtails␈αof␈α(A␈α
B␈αC␈αD)␈αare␈α(A␈αB␈αC␈αD),␈α
(B␈αC␈αD),␈α(C␈αD),␈α(D)␈αand␈α
NIL.␈α The
␈↓ α∧␈↓natural recursive definition of ␈↓↓istail␈↓ is

␈↓ α∧␈↓3)␈↓ αt ␈↓↓u istail v ← (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v)␈↓

␈↓ α∧␈↓which according to the previous sections would lead to the first order formula

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀u v.(u istail v ≡ (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v))␈↓,

␈↓ α∧␈↓but␈α
(4)␈α
is␈α
still␈α
an␈αimplicit␈α
definition␈α
of␈α
␈↓↓istail␈↓,␈α
because␈αthe␈α
function␈α
being␈α
defined␈α
occurs␈α
on␈αboth
␈↓ α∧␈↓sides of the equivalence sign.  A suitable explicit definition is

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀u v.(u istail v ≡ occur[u,v] ∧ ∀x.(occur[u,x] ∧ occur[x,v] ⊃ x = u ∨ occur[u, ␈↓αd␈↓↓ x]))␈↓.

␈↓ α∧␈↓Next we shall define membership in a list.  We have

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = ␈↓αa␈↓↓ u))␈↓.

␈↓ α∧␈↓Now we define an ␈↓↓a-list␈↓ - a familiar Lisp concept.  We have

␈↓ α∧␈↓7)␈↓ αt␈α␈↓↓∀w.(isalist␈αw␈α≡␈α∀x.(x␈αε␈αw␈α⊃␈α¬␈↓αa␈↓↓t␈αx)␈α∧␈α∀u1␈α
u2.(u1␈αistail␈αw␈α∧␈αu2␈αistail␈αw␈α∧␈α␈↓αaa␈↓↓␈αu1␈α=␈α␈↓αaa␈↓↓␈αu2␈α
⊃
␈↓ α∧␈↓↓u1 = u2))␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f15


␈↓ α∧␈↓Thus␈α∞an␈α
␈↓↓a-list␈↓␈α∞is␈α∞a␈α
list␈α∞of␈α
pairs␈α∞such␈α∞that␈α
no␈α∞S-expression␈α
is␈α∞the␈α∞first␈α
element␈α∞of␈α∞two␈α
different
␈↓ α∧␈↓pairs.␈α⊃ Therefore,␈α⊃a-lists␈α⊃are␈α⊃suitable␈α⊃for␈α⊂representing␈α⊃finite␈α⊃lists␈α⊃of␈α⊃argument-value␈α⊃pairs␈α⊂for
␈↓ α∧␈↓partial functions.

␈↓ α∧␈↓␈↓ αTFinally,␈α
we␈α
need␈α
the␈α
familiar␈α
Lisp␈α
function␈α
␈↓↓assoc␈↓␈α
that␈α
is␈α
used␈α
for␈α
looking␈α
up␈α
atoms␈α
on␈α␈↓↓a-
␈↓ α∧␈↓↓lists␈↓.  Its familiar recursive definition is

␈↓ α∧␈↓8)␈↓ αt ␈↓↓assoc(x,w) ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc(x,␈↓αd␈↓↓ w)␈↓,

␈↓ α∧␈↓but it can be represented by

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = ␈↓αa␈↓↓ w1) ∨ assoc(x,w) = ␈↓NIL␈↓↓)␈↓.

␈↓ α∧␈↓␈↓ αTNow let ␈↓↓f␈↓ be an arbitrary recursive program defined by

␈↓ α∧␈↓10)␈↓ αt ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ α∧␈↓for␈αsome␈αcontinuous␈α
functional␈α␈↓	t␈↓.␈α In␈αorder␈α
to␈αemphasize␈αthe␈αparallel␈α
between␈αa␈αpartial␈αfunction␈α
␈↓↓f␈↓
␈↓ α∧␈↓and an ␈↓↓a-list␈↓ used as a finite approximation, we define

␈↓ α∧␈↓11)␈↓ αt ␈↓	t␈↓↓'(w)(x) = ␈↓	t␈↓↓[λz.␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(z,w) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(z,w)](x)␈↓.

␈↓ α∧␈↓Thus␈α␈↓	t␈↓'␈αis␈αlike␈α␈↓	t␈↓␈αexcept␈α
that␈αwhenever␈α␈↓	t␈↓␈αevaluates␈αits␈αfunctional␈α
argument␈α␈↓↓f␈↓␈αat␈αsome␈αvalue␈α␈↓↓z,␈↓␈α
␈↓	t␈↓'
␈↓ α∧␈↓looks up ␈↓↓z␈↓ on the a-list ␈↓↓w.␈↓

␈↓ α∧␈↓␈↓ αTWith this preparation we can write

␈↓ α∧␈↓12)␈↓ αt␈α␈↓↓∀x␈α(¬∃y␈αw.(x.y␈α=␈α␈↓αa␈↓↓␈αw␈α∧␈α∀x1␈αy1␈αw1.(w1␈αistail␈αw␈α∧␈αx1.y1␈α=␈α␈↓αa␈↓↓␈αw1␈α⊃␈αy1␈α=␈α␈↓	t␈↓↓'[␈↓αd␈↓↓␈αw1](x1)))␈α⊃
␈↓ α∧␈↓↓f(x)␈α=␈α␈↓πT␈↓↓)␈α∧␈α
∀y.(∃w.(x.y␈α=␈α␈↓αa␈↓↓␈αw␈α∧␈α
∀x1␈αy1␈αw1.(w1␈αistail␈αw␈α
∧␈αx1.y1␈α=␈α␈↓αa␈↓↓␈αw1␈α
⊃␈αy1␈α=␈α␈↓	t␈↓↓'[␈↓αd␈↓↓␈α
w1](x1))))␈α⊃
␈↓ α∧␈↓↓f(x) = y))␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α∞essence␈α
of␈α∞this␈α
formula␈α∞is␈α
simple.␈α∞ ␈↓↓w␈↓␈α
is␈α∞an␈α
a-list␈α∞containing␈α
all␈α∞argument-value␈α
pairs
␈↓ α∧␈↓that␈α⊂arise␈α⊂in␈α⊂the␈α⊂evaluation␈α∂of␈α⊂␈↓↓f(x).␈↓␈α⊂We␈α⊂require␈α⊂that␈α⊂if␈α∂␈↓↓x␈↓␈α⊂occurs␈α⊂somewhere␈α⊂on␈α⊂␈↓↓w,␈↓␈α⊂the␈α∂pairs
␈↓ α∧␈↓involved␈α∂in␈α∂the␈α∂evaluation␈α∂of␈α∞␈↓↓f(x)␈↓␈α∂occur␈α∂further␈α∂on␈α∂in␈α∂the␈α∞a-list␈α∂␈↓↓w.␈↓␈α∂This␈α∂is␈α∂to␈α∂avoid␈α∞allowing
␈↓ α∧␈↓circular recursions.  If there is no such a-list, then ␈↓↓f(x) = ␈↓πT␈↓↓.

␈↓ α∧␈↓␈↓ αTIf␈α
the␈αlogic␈α
has␈α
a␈αdescription␈α
operator␈α
␈↓	i␈↓,␈αwhere␈α
␈↓	i␈↓↓␈α
x.P(x)␈↓␈αstands␈α
for␈α
the␈α"the␈α
unique␈α
␈↓↓x␈↓␈αsuch
␈↓ α∧␈↓that ␈↓↓P(x)␈↓ if there is such a unique ␈↓↓x␈↓ and otherwise ␈↓πT␈↓", then (12) can be written

␈↓ α∧␈↓13)␈↓ αt␈α∂␈↓↓∀x.(f(x)␈α∂=␈α∂␈↓	i␈↓↓␈α∂y.∃w.(x.y␈α∂=␈α∂␈↓αa␈↓↓␈α∞w␈α∂∧␈α∂∀x1␈α∂y1␈α∂w1.(w1␈α∂istail␈α∂w␈α∞∧␈α∂x1.y1␈α∂=␈α∂␈↓αa␈↓↓␈α∂w1␈α∂⊃␈α∂y1␈α∂=␈α∞␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ α∧␈↓↓w1](x1))))␈↓.

␈↓ α∧␈↓␈↓ αTAs an example, consider the Lisp function ␈↓↓ff␈↓ defined recursively by

␈↓ α∧␈↓14)␈↓ αt ␈↓↓ff x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ff ␈↓αa␈↓↓ x␈↓.

␈↓ α∧␈↓(13) then takes the form

␈↓ α∧␈↓15)␈↓ αt␈α
∀x.(ff␈αx␈α
=␈α␈↓	i␈↓↓y.∃w.(x.y␈α
=␈α
␈↓αa␈↓↓␈αw␈α
∧␈α∀x1␈α
y1␈α
w1.(w1␈αistail␈α
w␈α∧␈α
x1.y1␈α
=␈α␈↓αa␈↓↓␈α
w1␈α⊃␈α
y1␈α
=␈α␈↓αif␈↓↓␈α
␈↓αa␈↓↓t␈αx1␈α
␈↓αthen␈↓↓
␈↓ α∧␈↓↓x1 ␈↓αelse␈↓↓ (␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x1,␈↓αd␈↓↓ w1) ␈↓αthen␈↓↓ ␈↓πT␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x1,␈↓αd␈↓↓ w1)))))␈↓.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f16


␈↓ α∧␈↓␈↓ αTSuppose␈α∞we␈α∞were␈α∞computing␈α∞␈↓↓ff ((A.B).C)␈↓.␈α
 A␈α∞suitable␈α∞␈↓↓w␈↓␈α∞would␈α∞be␈α∞((((A.B).C).A)␈α
((A.B).A)
␈↓ α∧␈↓(A.A)).

␈↓ α∧␈↓␈↓ αTIt␈α∂might␈α∂be␈α⊂asked␈α∂whether␈α∂␈↓↓occur␈↓␈α∂is␈α⊂necessary.␈α∂ Couldn't␈α∂we␈α∂represent␈α⊂recursive␈α∂programs
␈↓ α∧␈↓using␈αjust␈α␈↓↓car,␈αcdr,␈αcons␈↓␈αand␈α␈↓↓atom␈↓?␈α No,␈αfor␈αthe␈αfollowing␈αreason.␈α Suppose␈αthat␈αthe␈αfunction␈α␈↓↓f␈↓␈αis
␈↓ α∧␈↓representable using only the basic Lisp functions without ␈↓↓subexp␈↓, and consider the sentence

␈↓ α∧␈↓16)␈↓ αt ␈↓↓∀x.issexp f(x)␈↓,

␈↓ α∧␈↓asserting␈αthe␈αtotality␈α
of␈α␈↓↓f.␈↓␈αUsing␈α
the␈αrepresentation,␈αwe␈α
can␈αwrite␈α(16)␈α
as␈αa␈αsentence␈αinvolving␈α
only
␈↓ α∧␈↓the␈α⊂basic␈α⊃Lisp␈α⊂functions␈α⊃and␈α⊂the␈α⊂constant␈α⊃␈↓πT␈↓.␈α⊂ However,␈α⊃may␈α⊂be␈α⊂shown␈α⊃in␈α⊂Appendix␈α⊃I,␈α⊂these
␈↓ α∧␈↓sentences␈αare␈αdecidable,␈αand␈αtotality␈αisn't.␈α (I'll␈αput␈αthe␈αproof␈αin␈αAppendix␈αI␈αif␈αI␈αcan␈αprove␈αit.␈α At
␈↓ α∧␈↓this time, I think I've almost got it).

␈↓ α∧␈↓␈↓ αTIn␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(12)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ α∧␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ α∧␈↓rules.␈α∞ The␈α∞difference␈α∂is␈α∞not␈α∞important,␈α∂because␈α∞of␈α∞Vuillemin's␈α∂theorem␈α∞that␈α∞any␈α∂strict␈α∞function
␈↓ α∧␈↓may be computed either according to call-by-name or call-by-value.


␈↓ α∧␈↓α9. Questions of Incompleteness.

␈↓ α∧␈↓␈↓ αTLuckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ α∧␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ α∧␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ α∧␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ α∧␈↓order representations?

␈↓ α∧␈↓␈↓ αTFirst␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ α∧␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
 We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ α∧␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ α∧␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
 Assuming␈αthe␈α
axioms
␈↓ α∧␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ α∧␈↓the␈α⊂program␈α⊂will␈α⊂never␈α⊂stop␈α⊂is␈α⊃precisely␈α⊂proving␈α⊂that␈α⊂the␈α⊂axioms␈α⊂are␈α⊂consistent.␈α⊃ But␈α⊂G␈↓
:␈↓odel's
␈↓ α∧␈↓theorem␈αasserts␈αthat␈αaxiom␈αsystems␈αlike␈αLisp1␈αcannot␈αbe␈αproved␈αconsistent␈αwithin␈αthemselves.␈α All
␈↓ α∧␈↓the␈αknown␈αcases␈αof␈αterminating␈αcomputations␈αthat␈αcan't␈αbe␈αproved␈αnot␈αto␈αterminate␈αwithin␈αPeano
␈↓ α∧␈↓arithmetic involve such an appeal to G␈↓
:␈↓odel's theorem or similar unsolvability arguments.

␈↓ α∧␈↓␈↓ αTWe␈α
can␈α
presumably␈α
prove␈α
Lisp1␈α
consistent␈α
just␈α
as␈α
Gentzen␈α
proved␈α
arithmetic␈α∞consistent␈α
-
␈↓ α∧␈↓by␈α∩introducing␈α∪a␈α∩new␈α∩axiom␈α∪schema␈α∩that␈α∩allows␈α∪induction␈α∩up␈α∩to␈α∪the␈α∩transfinite␈α∪ordinal␈α∩ε␈↓β0␈↓.
␈↓ α∧␈↓Proving the new system consistent would require induction up to a still higher ordinal, etc.

␈↓ α∧␈↓␈↓ αTSince␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ α∧␈↓such␈αfunctions␈αcan␈αbe␈αreplaced␈αby␈αan␈αequivalent␈αsentence␈αinvolving␈αonly␈α␈↓↓occur␈↓␈αand␈αthe␈αbasic␈αLisp
␈↓ α∧␈↓functions.␈α The␈αtheory␈αof␈α
␈↓↓occur␈↓␈αand␈αthese␈αfunctions␈αhas␈α
a␈αstandard␈αmodel,␈αthe␈αusual␈α
S-expressions
␈↓ α∧␈↓and␈α∪many␈α∩non-standard␈α∪models.␈α∩ We␈α∪"construct"␈α∩non-standard␈α∪models␈α∩in␈α∪the␈α∩usual␈α∪way␈α∩by
␈↓ α∧␈↓appealing␈α
to␈α
the␈α
theorem␈α
that␈α
if␈α
every␈α
finite␈α
subset␈α
of␈α
a␈α
set␈α
␈↓↓S␈↓␈α
of␈α
sentences␈α
of␈α
first␈α
order␈α
logic␈αhas␈α
a
␈↓ α∧␈↓model,␈αthen␈α␈↓↓S␈↓␈αhas␈αa␈αmodel.␈α For␈αexample,␈αtake␈α␈↓↓S␈α=␈α{occur[␈↓NIL␈↓↓,␈αx],␈αoccur[␈↓(A)␈↓↓,␈αx],␈αoccur[␈↓(A␈αA)␈↓↓␈α,
␈↓ α∧␈↓↓x],␈α...␈↓␈αindefinitely}.␈α Every␈αfinite␈αsubset␈αof␈α␈↓↓S␈↓␈αhas␈αa␈αmodel;␈αwe␈αneed␈αonly␈αtake␈α␈↓↓x␈↓␈αto␈αbe␈αthe␈αlongest
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f17


␈↓ α∧␈↓list␈αof␈αA's␈αoccurring␈αin␈αthe␈αsentences.␈α Hence␈αthere␈αis␈αa␈αmodel␈αof␈αthe␈αLisp␈αaxioms␈αin␈αwhich␈α␈↓↓x␈↓␈αhas
␈↓ α∧␈↓all␈α∞lists␈α∂of␈α∞A's␈α∞as␈α∂subexpressions.␈α∞ No␈α∞sentence␈α∂true␈α∞in␈α∞the␈α∂standard␈α∞model␈α∞and␈α∂false␈α∞in␈α∂such␈α∞a
␈↓ α∧␈↓model␈αcan␈αbe␈αproved␈αfrom␈αthe␈αaxioms.␈α However,␈αit␈αis␈αnecessary␈αto␈αbe␈αcareful␈αabout␈αthe␈αmeaning
␈↓ α∧␈↓of␈αtermination␈αof␈αa␈αfunction.␈α
 In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈α
of␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈α
never␈αterminate,
␈↓ α∧␈↓but␈α
the␈αsentence␈α
whose␈α␈↓↓standard␈α
interpretation␈↓␈αis␈α
termination␈αof␈α
the␈αcomputation␈α
is␈αprovable␈α
from
␈↓ α∧␈↓Lisp1.

␈↓ α∧␈↓␈↓ αTThe␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ α∧␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
 It␈αdoesn't
␈↓ α∧␈↓follow␈α
that␈α
the␈α
system␈α
Lisp1␈α
will␈α∞permit␈α
convenient␈α
proofs,␈α
but␈α
probably␈α
it␈α
will.␈α∞ Some␈α
heuristic
␈↓ α∧␈↓evidence␈α
for␈α
this␈α
comes␈α
from␈α
(Cohen␈α
1965).␈α
 Cohen␈α
presents␈α
two␈α
systems␈α
of␈α
axiomatized␈α
arithmetic
␈↓ α∧␈↓Z1␈α
and␈α
Z2.␈α
 Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ α∧␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ α∧␈↓but␈αbecause␈αthe␈αset␈αoperations␈αof␈αZ2␈αcan␈αbe␈αrepresented␈αin␈αZ1␈αas␈αfunctions␈αon␈αthe␈αG␈↓
:␈↓odel␈αnumbers
␈↓ α∧␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ α∧␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ α∧␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ α∧␈↓should␈α
be␈αpossible.␈α
 Moreover,␈α
since␈αLisp1␈α
is␈αa␈α
first␈α
order␈αtheory,␈α
it␈α
is␈αeasily␈α
extended␈αwith␈α
axioms
␈↓ α∧␈↓for␈α
sets,␈αand␈α
this␈α
should␈αhelp␈α
make␈α
informal␈αproofs␈α
easy␈αto␈α
express.␈α
 It␈αwould␈α
be␈α
nice␈αto␈α
be␈αable␈α
to
␈↓ α∧␈↓express these considerations less vaguely.


␈↓ α∧␈↓α10. References.

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ α∧␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.

␈↓ α∧␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ α∧␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

␈↓ α∧␈↓␈↓αKleene, S.C. (1951)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.

␈↓ α∧␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ α∧␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).

␈↓ α∧␈↓␈↓αManna,␈αZohar␈αand␈α
Amir␈αPnueli␈α(1970)␈↓:␈α
"Formalization␈αof␈αthe␈α
Properties␈αof␈αFunctional␈α
Programs",
␈↓ α∧␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.

␈↓ α∧␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.

␈↓ α∧␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ α∧␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).

␈↓ α∧␈↓␈↓αMcCarthy,␈αJohn␈↓␈α(1963)␈α"A␈α
Basis␈αfor␈αa␈αMathematical␈αTheory␈α
of␈αComputation",␈αin␈αP.␈αBraffort␈α
and
␈↓ α∧␈↓D.␈α⊃Hirschberg␈α⊃(eds.),␈α⊂␈↓↓Computer␈α⊃Programming␈α⊃and␈α⊂Formal␈α⊃Systems␈↓,␈α⊃pp.␈α⊃33-70.␈α⊂ North-Holland
␈↓ α∧␈↓Publishing Company, Amsterdam.
␈↓ α∧␈↓REPRESENTATION␈↓ εR...draft...␈↓ f18


␈↓ α∧␈↓␈↓αMorris,␈α
James␈αH.,␈α
and␈αBen␈α
Wegbreit␈α
(1977)␈↓:␈α"Program␈α
Verification␈αby␈α
Subgoal␈αInduction",␈α
␈↓↓Comm.
␈↓ α∧␈↓↓ACM␈↓,␈↓α20␈↓(4): 209-222 (April).

␈↓ α∧␈↓␈↓αPark,␈α_David␈α_(1969)␈↓:␈α_Fixpoint␈α_Induction␈α_and␈α_Proofs␈α_of␈α_Program␈α_Properties",␈α_in␈α↔␈↓↓Machine
␈↓ α∧␈↓↓Intelligence 5␈↓, pp. 59-78, Edinburgh University Press, Edinburgh.

␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305

␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI